(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 2))
(let ((e4 0))
(let ((e5 13))
(let ((e6 (+ v2 v1)))
(let ((e7 (- v0 e6)))
(let ((e8 (+ e6 v0)))
(let ((e9 (- e6)))
(let ((e10 (- e8)))
(let ((e11 (* (- e5) e7)))
(let ((e12 (- e10)))
(let ((e13 (- v2 e6)))
(let ((e14 (- v0 e10)))
(let ((e15 (* e9 e9)))
(let ((e16 (/ e3 e3)))
(let ((e17 (- e16)))
(let ((e18 (+ v1 e14)))
(let ((e19 (- e9)))
(let ((e20 (/ e4 (- e5))))
(let ((e21 (distinct e9 e12)))
(let ((e22 (<= e9 v0)))
(let ((e23 (distinct e13 e18)))
(let ((e24 (= e10 e10)))
(let ((e25 (>= e7 e12)))
(let ((e26 (> e6 e11)))
(let ((e27 (= e14 e7)))
(let ((e28 (= e8 e12)))
(let ((e29 (= e15 e17)))
(let ((e30 (= e12 e11)))
(let ((e31 (> v2 e19)))
(let ((e32 (= e10 e11)))
(let ((e33 (< e13 e10)))
(let ((e34 (>= e8 e7)))
(let ((e35 (distinct e12 e10)))
(let ((e36 (>= e16 e15)))
(let ((e37 (> e12 e20)))
(let ((e38 (>= e14 e15)))
(let ((e39 (distinct e9 e17)))
(let ((e40 (<= e17 e18)))
(let ((e41 (> e20 e13)))
(let ((e42 (= e12 e7)))
(let ((e43 (< e19 e16)))
(let ((e44 (> e19 e17)))
(let ((e45 (> e20 e8)))
(let ((e46 (distinct v0 e19)))
(let ((e47 (>= e9 e19)))
(let ((e48 (distinct e13 e18)))
(let ((e49 (>= e20 e18)))
(let ((e50 (= v1 e7)))
(let ((e51 (> e12 e9)))
(let ((e52 (> e16 e7)))
(let ((e53 (> e6 e7)))
(let ((e54 (<= e19 v1)))
(let ((e55 (distinct v1 e12)))
(let ((e56 (= e7 e16)))
(let ((e57 (<= e14 e18)))
(let ((e58 (distinct v2 e17)))
(let ((e59 (>= e17 v1)))
(let ((e60 (<= e9 e11)))
(let ((e61 (>= e13 e12)))
(let ((e62 (<= e7 e14)))
(let ((e63 (distinct v1 e12)))
(let ((e64 (= e18 e15)))
(let ((e65 (= v2 e8)))
(let ((e66 (>= v0 e15)))
(let ((e67 (= e8 e19)))
(let ((e68 (>= e15 e9)))
(let ((e69 (distinct e15 e20)))
(let ((e70 (> e11 e7)))
(let ((e71 (> e6 e10)))
(let ((e72 (=> e52 e41)))
(let ((e73 (and e34 e58)))
(let ((e74 (xor e71 e60)))
(let ((e75 (xor e65 e27)))
(let ((e76 (= e75 e47)))
(let ((e77 (xor e56 e63)))
(let ((e78 (and e29 e64)))
(let ((e79 (=> e62 e28)))
(let ((e80 (=> e22 e70)))
(let ((e81 (and e31 e72)))
(let ((e82 (not e26)))
(let ((e83 (not e57)))
(let ((e84 (and e67 e77)))
(let ((e85 (or e78 e38)))
(let ((e86 (and e30 e55)))
(let ((e87 (=> e25 e74)))
(let ((e88 (=> e68 e51)))
(let ((e89 (= e21 e40)))
(let ((e90 (ite e80 e49 e85)))
(let ((e91 (= e66 e46)))
(let ((e92 (and e44 e54)))
(let ((e93 (not e61)))
(let ((e94 (xor e76 e50)))
(let ((e95 (not e35)))
(let ((e96 (xor e82 e45)))
(let ((e97 (and e23 e69)))
(let ((e98 (ite e86 e95 e48)))
(let ((e99 (xor e73 e97)))
(let ((e100 (not e24)))
(let ((e101 (= e36 e96)))
(let ((e102 (or e92 e83)))
(let ((e103 (or e99 e91)))
(let ((e104 (=> e37 e98)))
(let ((e105 (xor e103 e103)))
(let ((e106 (= e39 e81)))
(let ((e107 (xor e79 e43)))
(let ((e108 (and e84 e104)))
(let ((e109 (= e59 e59)))
(let ((e110 (=> e88 e42)))
(let ((e111 (= e105 e105)))
(let ((e112 (or e109 e32)))
(let ((e113 (ite e102 e53 e100)))
(let ((e114 (and e93 e113)))
(let ((e115 (=> e114 e106)))
(let ((e116 (= e111 e89)))
(let ((e117 (= e94 e94)))
(let ((e118 (=> e108 e101)))
(let ((e119 (or e107 e112)))
(let ((e120 (=> e90 e115)))
(let ((e121 (= e116 e118)))
(let ((e122 (ite e33 e119 e119)))
(let ((e123 (or e121 e117)))
(let ((e124 (xor e120 e87)))
(let ((e125 (=> e122 e124)))
(let ((e126 (=> e123 e123)))
(let ((e127 (not e125)))
(let ((e128 (and e127 e126)))
(let ((e129 (and e128 e110)))
e129
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
